COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	axiom stepdef:	∀j.(phi1(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m*(n - i(t))
C00003 ENDMK
C⊗;
axiom stepdef:	∀j.(phi1(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m*(n - i(t))
	∧ i(t) = j)
		⊃ ∃t.(pc(t) = done ∧ p(t) = m*n));;

∧i stepdef[phi←λj.phi1(j)];